es:ES, ff:FIFO, is_req, is_ack:(E), awaiting, owes_ack:(IdIdId).
(ff.C r Id)
 (i, j:ff.C. @i(awaiting(i,j):) & @i(owes_ack(i,j):))
 (i:ff.C, e:E. (ff.R(i,e))  (loc(e) = i  Id))
 (e:E. Dec(is_req(e)) & Dec(is_ack(e)))
 (i, j:ff.C, e:E. Dec(ff.S(i,j,e)))
 (i, j:ff.C, e:E. (ff.S(i,j,e))  (loc(e) = i  Id))
 plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack)
 (sndr, rcvr:ff.C, e:E.
 (loc(e) = rcvr  Id)
  ((owes_ack(rcvr,sndr) when e) = ff  )
  ((owes_ack(rcvr,sndr) after e) = tt  )
  [e: rcvr is_req sndr]) 

latex

Definitions	{T}, SQType(T), t  T, A c B, A, [e: i p j], P & Q, P  Q, , x:A. B(x), P  Q, False, P  Q, [e: i p j], plus-ify{i:l}(es;ff;is_req;is_ack;awaiting;owes_ack), @i(x:T)
Lemmas	event system wf, FIFO wf, Id wf, fifoC wf, es-dtype wf, fifoR wf, es-E wf, decidable wf, fifoS wf, plus-ify wf, es-loc wf, es-when wf, Id sq, es-after wf, bool wf, inconsistent-bool-eq